/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=BDJ20/FONT#10=BDJ20
␈↓ α∧␈↓␈↓ u1


















␈↓ α∧␈↓α␈↓ α*THE ELEPHANT LANGUAGE FOR PROVING AND MAYBE EVEN PROGRAMMING

␈↓ α∧␈↓␈↓ ελby John McCarthy

␈↓ α∧␈↓␈↓αAbstract:␈↓␈αAn␈αElephant␈αprogram␈αis␈αa␈αcollection␈αof␈αsentences␈αof␈αfirst␈αorder␈αlogic.␈α Corresponding␈αto
␈↓ α∧␈↓a␈αprogram␈αvariable␈α
␈↓↓x␈↓␈αin␈αan␈α
Algol-type␈αprogram,␈αthere␈αis␈α
a␈αfunction␈α␈↓↓x(t)␈↓␈α
of␈αtime␈αin␈α
the␈αElephant
␈↓ α∧␈↓program.␈α
 Sentences␈α∞of␈α
first␈α∞order␈α
logic␈α∞tell␈α
how␈α
the␈α∞values␈α
of␈α∞variables␈α
like␈α∞␈↓↓x(t)␈↓␈α
depend␈α∞on␈α
the
␈↓ α∧␈↓values of the variables at earlier times.  The ␈↓↓program counter␈↓ is treated as just another variable.

␈↓ α∧␈↓␈↓ αTRepresenting␈αprogram␈αvariables␈αas␈αexplicit␈αfunctions␈αof␈αtime␈αhas␈αbeen␈αexplicitly␈αrejected␈αby
␈↓ α∧␈↓many␈α∞computer␈α∞scientists,␈α∞but␈α∞it␈α∞has␈α∞advantages␈α∞that␈α∞justify␈α∞overcoming␈α∞their␈α∂prejudices.␈α∞ First,
␈↓ α∧␈↓properties␈αof␈α
Elephant␈αprograms␈α
are␈αexpressed␈α
as␈αfirst␈α
order␈αsentences␈α
in␈αthe␈α
language␈αof␈αthe␈α
data
␈↓ α∧␈↓domain␈α
augmented␈αby␈α
the␈α
names␈αof␈α
the␈αfunctions␈α
constituting␈α
the␈αprogram.␈α
 The␈α
usual␈αmethods
␈↓ α∧␈↓for␈αproving␈αproperties␈αof␈αprograms␈αrequire␈αno␈αnew␈α"logic␈αof␈αprogramming";␈αthey␈αare␈αjust␈αstyles␈αof
␈↓ α∧␈↓proof␈α
in␈α
first␈α
order␈α
logic.␈α
 Except␈α
in␈α
exotic␈α
cases,␈α
when␈α
the␈α
sentences␈α
we␈α
want␈α
to␈α
prove␈α
fail␈α
in␈α
non-
␈↓ α∧␈↓standard␈αmodels␈αof␈α
arithmetic,␈αall␈αproperties␈α
of␈αprograms␈αare␈α
logical␈αconsequences␈αof␈αthe␈α
sentences
␈↓ α∧␈↓expressing␈α∂the␈α∂Elephant␈α∂program␈α∂and␈α∂the␈α∞axioms␈α∂of␈α∂the␈α∂data␈α∂domain.␈α∂ We␈α∂make␈α∞comparisons
␈↓ α∧␈↓with␈α∩temporal␈α∩logic.␈α∩ Second,␈α∩equivalences␈α⊃between␈α∩programs␈α∩are␈α∩conveniently␈α∩expressed␈α⊃and
␈↓ α∧␈↓proved.␈α
 Third,␈α
the␈α
sentence␈α
representing␈α
a␈α
combination␈α
of␈α
flowcharts␈α
is␈α
just␈α
the␈α
conjunction␈αof
␈↓ α∧␈↓the sentences representing the flowcharts separately.

␈↓ α∧␈↓␈↓ αTBesides␈α⊃representing␈α∩ordinary␈α⊃sequential␈α⊃and␈α∩parallel␈α⊃programs,␈α⊃Elephant␈α∩can␈α⊃represent
␈↓ α∧␈↓programs␈α
that␈α∞refer␈α
to␈α
the␈α∞past␈α
of␈α
variables␈α∞and␈α
therefore␈α
avoid␈α∞explicit␈α
mention␈α
of␈α∞many␈α
data
␈↓ α∧␈↓structures.␈α∪ Since␈α∪we␈α∪often␈α∪refer␈α∪to␈α∪the␈α∪past␈α∪in␈α∪expressing␈α∪processes␈α∪in␈α∪natural␈α∪language,␈α∪a
␈↓ α∧␈↓computer language that doesn't allow it cannot claim to be "natural".
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u2


␈↓ α∧␈↓1. ␈↓αIntroduction␈↓

␈↓ α∧␈↓␈↓ αTThe␈α⊂Elephant␈α⊂algorithmic␈α∂language␈α⊂represents␈α⊂program␈α⊂variables␈α∂as␈α⊂functions␈α⊂of␈α⊂a␈α∂time

␈↓ α∧␈↓variable␈α␈↓↓t␈↓.␈α Instead␈αof␈αa␈αvariable␈α␈↓↓x␈↓␈αas␈αin␈αan␈αAlgol␈αprogram,␈αan␈αElephant␈αprogram␈αhas␈αa␈αfunction

␈↓ α∧␈↓␈↓↓x(t),␈↓␈α∂and␈α∂instead␈α∂of␈α∂an␈α∂assignment␈α∂statement␈α∂␈↓↓x := ...␈↓,␈α∂we␈α∂may␈α∂use␈α∂an␈α∂equation␈α∂␈↓↓x(t+1) = ...␈↓␈α∂or

␈↓ α∧␈↓sometimes ␈↓↓x(t) = ...␈↓.  This formalism has two uses.

␈↓ α∧␈↓␈↓ αTFirst,␈α
Elephant␈α
provides␈α
a␈αsimple␈α
way␈α
of␈α
expressing␈αsequential␈α
programs␈α
as␈α
sentences␈α
in␈αa

␈↓ α∧␈↓first␈αorder␈αtheory␈αwhich␈αcan␈αthen␈αbe␈αused␈αto␈αprove␈αproperties␈αof␈αthe␈αprogram.␈α This␈αcomplements

␈↓ α∧␈↓the␈α↔first␈α_order␈α↔representation␈α_of␈α↔recursive␈α_programs␈α↔described␈α_in␈α↔(Cartwright␈α_1976)␈α↔and

␈↓ α∧␈↓(Cartwright␈α∞and␈α∂McCarthy␈α∞1979)␈α∞in␈α∂that␈α∞an␈α∞Elephant␈α∂program␈α∞describes␈α∞what␈α∂is␈α∞to␈α∂happen␈α∞at

␈↓ α∧␈↓successive␈α∩times␈α∩starting␈α⊃with␈α∩the␈α∩initial␈α⊃state,␈α∩while␈α∩a␈α⊃recursive␈α∩description␈α∩describes␈α∩how␈α⊃a

␈↓ α∧␈↓desired␈α
function␈α
is␈α
computed␈α
with␈αthe␈α
help␈α
its␈α
values␈α
for␈αsimpler␈α
sets␈α
of␈α
arguments.␈α
 One␈αmight

␈↓ α∧␈↓say that Elephant is bottom-up while recursive programs are top-down.

␈↓ α∧␈↓␈↓ αTOnce␈α∞a␈α∞program␈α∞has␈α
been␈α∞expressed␈α∞in␈α∞Elephant,␈α
the␈α∞␈↓↓inductive␈α∞assertion␈↓␈α∞and␈α
␈↓↓intermittent

␈↓ α∧␈↓↓assertion␈↓␈α∂methods␈α∞are␈α∂automatically␈α∂available␈α∞as␈α∂particular␈α∂techniques␈α∞of␈α∂making␈α∂proofs␈α∞within

␈↓ α∧␈↓first␈α∀order␈α∀logic.␈α∀ They␈α∀amount␈α∀to␈α∀using␈α∀particular␈α∀kinds␈α∀of␈α∀lemmas␈α∀in␈α∀proving␈α∀theorems.

␈↓ α∧␈↓Instances of the Hoare axioms are also just lemmas.

␈↓ α∧␈↓␈↓ αTThe␈α
second␈α
aspect␈α
of␈α
Elephant␈α
(the␈α
motivation␈α
for␈α
the␈α
name)␈α
is␈α
the␈α
ability␈α
to␈α
refer␈α
to␈αthe

␈↓ α∧␈↓whole␈α∞past␈α∞of␈α∞the␈α∞variables␈α∞without␈α∞specifying␈α∞data␈α∞structures␈α∞for␈α∞remembering␈α∞what␈α∞has␈α∂to␈α∞be

␈↓ α∧␈↓known␈α
in␈αorder␈α
to␈αperform␈α
a␈αcurrent␈α
action.␈α Thus␈α
a␈αreservation␈α
program␈αwritten␈α
in␈αElephant␈α
can

␈↓ α∧␈↓say␈α∞that␈α∞a␈α∞passenger␈α∞has␈α∞a␈α∞reservation␈α∞if␈α
he␈α∞has␈α∞made␈α∞one␈α∞and␈α∞not␈α∞cancelled␈α∞it.␈α∞ The␈α
program

␈↓ α∧␈↓needn't␈α∩specify␈α∩any␈α∩data␈α∩structure␈α∩for␈α⊃remembering␈α∩who␈α∩has␈α∩reservations;␈α∩␈↓↓an␈α∩elephant␈α⊃never

␈↓ α∧␈↓↓forgets␈↓.␈α∞ Likewise,␈α∞the␈α∞rule␈α∞that␈α∞a␈α∞castling␈α∞move␈α∞is␈α∞prohibited␈α∞if␈α∞the␈α∞rook␈α∞or␈α∞king␈α∞involved␈α∞has

␈↓ α∧␈↓ever moved is directly expressible without inventing a variable to hold the information.

␈↓ α∧␈↓␈↓ αTSuch␈α∂reference␈α∂to␈α∂the␈α∞past␈α∂is␈α∂certainly␈α∂used␈α∂in␈α∞informal␈α∂English␈α∂descriptions␈α∂of␈α∂what␈α∞we
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u3


␈↓ α∧␈↓want␈αa␈αcomputer␈αto␈αdo.␈α Therefore,␈αa␈αsufficiently␈αhigh␈αlevel␈αprogramming␈αlanguage␈αmust␈αhave␈αit.

␈↓ α∧␈↓On␈α
the␈αother␈α
hand,␈αthe␈α
Elephant␈αprograms␈α
that␈αI␈α
have␈αbeen␈α
able␈αto␈α
write␈αthat␈α
refer␈αto␈α
the␈αpast

␈↓ α∧␈↓are␈αoften␈αmore␈αdifficult␈αto␈αwrite␈αand␈αread␈αthan␈αprograms␈αwith␈αexplicit␈αdata␈αstructures.␈α Perhaps␈αI

␈↓ α∧␈↓am␈α
simply␈α
inexperienced␈α
in␈αwriting␈α
Elephant␈α
program,␈α
but␈αmost␈α
likely␈α
extensions␈α
to␈αthe␈α
formalism

␈↓ α∧␈↓are␈α∞also␈α∞needed.␈α∞ Of␈α∞course,␈α∞there␈α∞is␈α∞no␈α∞more␈α∞reason␈α∞to␈α∞make␈α∞a␈α∞fetish␈α∞out␈α∞not␈α∞mentioning␈α
data

␈↓ α∧␈↓structures than of not mentioning time.

␈↓ α∧␈↓␈↓ αTThe simplest way to begin is with examples.



␈↓ α∧␈↓2. ␈↓αExpressing a sequential program in Elephant␈↓

␈↓ α∧␈↓␈↓ αTConsider␈α⊗the␈α⊗following␈α⊗Algol␈α⊗60␈α⊗program␈α⊗fragment␈α⊗(declarations␈α⊗omitted)␈α↔for␈α⊗doing

␈↓ α∧␈↓multiplication by iterated addition:

␈↓ α∧␈↓↓start:  i := n;␈↓ ¬T0
␈↓ α∧␈↓↓␈↓ αTp := 0;␈↓ ¬T1
␈↓ α∧␈↓↓loop:   ␈↓αif␈↓↓ i = 0 ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;␈↓ ¬T2
␈↓ α∧␈↓↓␈↓ αTi := i - 1;␈↓ ¬T3
␈↓ α∧␈↓↓␈↓ αTp := p + m;␈↓ ¬T4
␈↓ α∧␈↓↓␈↓ αT␈↓αgo to␈↓↓ loop;␈↓ ¬T5

␈↓ α∧␈↓↓done:

␈↓ α∧␈↓One way of writing a corresponding Elephant program consists of the sentences

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = start + 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start + 5 THEN i(t)
␈↓ α∧␈↓↓␈↓ β4ELSE i(t+1)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start + 1 THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = start + 4 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start + 5 THEN p(t)
␈↓ α∧␈↓↓␈↓ β4ELSE p(t+1)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = start + 5 THEN start + 2
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start + 5 THEN pc(t) + 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t+1)].
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u4


␈↓ α∧␈↓␈↓ αTIn␈α
these␈α∞equations␈α
␈↓↓i(t)␈↓␈α
and␈α∞␈↓↓p(t)␈↓␈α
replace␈α∞the␈α
variables␈α
␈↓↓i␈↓␈α∞and␈α
␈↓↓p␈↓␈α
of␈α∞the␈α
Algol␈α∞program.␈α
 The

␈↓ α∧␈↓function␈α
␈↓↓pc(t)␈↓␈α
is␈α
the␈α
program␈α
counter,␈α
and␈α
it␈α
takes␈α
values␈α
from␈α
␈↓↓start␈↓␈α
to␈α
␈↓↓start+5␈↓␈α
assuming␈α∞that␈α
it

␈↓ α∧␈↓takes␈α
the␈αvalue␈α
␈↓↓start␈↓␈αfor␈α
some␈αvalue␈α
of␈α
␈↓↓t␈↓.␈α These␈α
match␈αthe␈α
numbers␈αwritten␈α
on␈αthe␈α
right␈α
of␈αthe

␈↓ α∧␈↓Algol␈αprogram.␈α
 Notice␈αthat␈α
the␈αsentences␈α
say␈αnothing␈α
about␈αthe␈α
values␈αof␈α
any␈αof␈α
the␈αvariables␈α
for

␈↓ α∧␈↓values␈α∞of␈α
␈↓↓pc(t)␈↓␈α∞outside␈α
the␈α∞range␈α
␈↓↓start␈↓␈α∞to␈α
␈↓↓start+5␈↓.␈α∞ This␈α
permits␈α∞these␈α
values␈α∞to␈α
be␈α∞described␈α
by

␈↓ α∧␈↓other sets of Elephant sentences.

␈↓ α∧␈↓␈↓ αTIt␈α∂should␈α∞be␈α∂apparent␈α∞from␈α∂the␈α∞example␈α∂that␈α∞any␈α∂program␈α∞made␈α∂up␈α∞of␈α∂assignments␈α∞and

␈↓ α∧␈↓␈↓αgo to␈↓s can be systematically translated to an Elephant program.

␈↓ α∧␈↓␈↓ αTNotice␈α∞also␈α∞that␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Elephant␈α∞program␈α∂is␈α∞linear␈α∞in␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Algol

␈↓ α∧␈↓program.

␈↓ α∧␈↓␈↓ αTHaving␈αone␈α
value␈αof␈α␈↓↓pc(t)␈↓␈α
for␈αeach␈αstatement␈α
in␈αthe␈αAlgol␈α
program␈αis␈αunnecessary,␈α
although

␈↓ α∧␈↓it␈α⊂makes␈α∂the␈α⊂systematic␈α⊂character␈α∂of␈α⊂the␈α∂correspondence␈α⊂more␈α⊂apparent.␈α∂ If␈α⊂we␈α⊂let␈α∂␈↓↓pc(t) = start␈↓

␈↓ α∧␈↓correspond␈α⊂to␈α⊂the␈α⊂initialization␈α⊂and␈α⊂␈↓↓pc(t) = start+1␈↓␈α⊂correspond␈α⊂to␈α⊂the␈α⊂loop,␈α⊂then␈α⊃the␈α⊂equations

␈↓ α∧␈↓become

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start+1 THEN i(t)
␈↓ α∧␈↓↓␈↓ β4ELSE i(t+1)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start+1 THEN p(t)
␈↓ α∧␈↓↓␈↓ β4ELSE p(t+1)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = start+1 THEN (IF i(t) = 0 THEN done ELSE start+1)
␈↓ α∧␈↓↓␈↓ β4ELSE IF start ≤ pc(t) ≤ start+1 THEN pc(t) + 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t+1)].

␈↓ α∧␈↓␈↓ αTThat these programs compute the product of ␈↓↓m␈↓ and ␈↓↓n␈↓ is specified by the sentence

␈↓ α∧␈↓␈↓ αT␈↓↓∀t0.[pc(t0) = start ⊃ ∃t.[t ≥ t0 ∧ pc(t) = done ∧ p(t) = m*n]]␈↓.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u5


␈↓ α∧␈↓It␈α∩is␈α∩provable␈α∩from␈α∩any␈α∩first␈α∩order␈α∩axiomatization␈α∩of␈α∩arithmetic␈α∩together␈α∩with␈α∩the␈α⊃sentences

␈↓ α∧␈↓constituting␈α∂the␈α⊂program.␈α∂ No␈α∂special␈α⊂axioms␈α∂for␈α⊂programs␈α∂or␈α∂"logic␈α⊂of␈α∂programs"␈α⊂is␈α∂required.

␈↓ α∧␈↓One need only apply mathematical induction to the predicate

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m(n - i(t)) ∧ i(t) = j ⊃ ∃t.(pc(t) = done ∧ p(t) = mn)␈↓

␈↓ α∧␈↓The␈α
case␈α␈↓↓j␈α
=␈α0␈↓␈α
follows␈αfrom␈α
the␈αequation␈α
for␈α
␈↓↓pc(t+1),␈↓␈αand␈α
the␈αinduction␈α
step␈αalso␈α
follows␈αfrom␈α
the

␈↓ α∧␈↓Elephant␈αprogram.␈α The␈αdesired␈α
result␈αis␈αthe␈αconclusion␈αof␈α
␈↓↓␈↓	F␈↓↓(n)␈↓,␈αand␈αthe␈αpremiss␈αof␈α
␈↓↓␈↓	F␈↓↓(n)␈↓␈αfollows

␈↓ α∧␈↓from the initial conditions.

␈↓ α∧␈↓␈↓ αTThus␈α
an␈α
entirely␈α
conventional␈α
mathematical␈α
way␈α
of␈α
writing␈α
recursion␈α
equations␈α
leads␈α∞to␈α
a

␈↓ α∧␈↓convenient␈αprogramming␈αlanguage.␈α It␈αis␈αtempting␈αto␈αcall␈αthe␈αlanguage␈αAlgol␈α50,␈αsince␈αit␈αonly␈αuses

␈↓ α∧␈↓ideas that were familiar in 1950.

␈↓ α∧␈↓␈↓ αTThe␈α
proof␈α
of␈α
correctness␈α
for␈α
this␈αmultiplication␈α
program␈α
is␈α
misleadingly␈α
simple,␈α
since␈αwe␈α
can

␈↓ α∧␈↓easily␈αwrite␈αexplicit␈αformulas␈αfor␈α␈↓↓i(t),␈↓␈α␈↓↓p(t),␈↓␈αand␈α␈↓↓pc(t)␈↓␈αand␈αprove␈αthem␈αby␈αmathematical␈αinduction.

␈↓ α∧␈↓Typically␈α⊃proofs␈α⊃will␈α⊃be␈α⊃required␈α⊃in␈α⊃which␈α⊃it␈α⊃isn't␈α⊃possible␈α⊃to␈α⊃give␈α⊃explicit␈α⊃formulas␈α⊃for␈α⊃the

␈↓ α∧␈↓variables␈αas␈αfunctions␈αof␈αtime␈αor␈αfor␈αthe␈αvalue␈αof␈α␈↓↓t␈↓␈αfor␈αwhich␈αthe␈αprogram␈αterminates.␈α Then␈αthe

␈↓ α∧␈↓computational␈α
content␈α
of␈α
the␈α
proof␈α
is␈α
is␈α
often␈α
essentially␈α
the␈α
same␈α
as␈α
that␈α
of␈α
an␈α␈↓↓inductive␈α
assertions␈↓

␈↓ α∧␈↓proof␈α∞combined␈α∞with␈α∞induction␈α∞on␈α∞a␈α∞rank␈α
function␈α∞of␈α∞the␈α∞variables␈α∞taking␈α∞values␈α∞in␈α∞a␈α
suitable

␈↓ α∧␈↓inductively ordered set.




␈↓ α∧␈↓3. ␈↓αReversing a list␈↓

␈↓ α∧␈↓␈↓ αTReversing␈α
a␈α
list␈α
provides␈α
another␈α
example␈αof␈α
an␈α
Elephant␈α
program␈α
that␈α
can␈α
be␈αcompared

␈↓ α∧␈↓with␈α∂a␈α∂recursive␈α∂conditional␈α∂expression␈α∂program␈α∂for␈α∂the␈α∂same␈α∂function.␈α∂ We␈α∂start␈α∂with␈α⊂a␈α∂Lisp

␈↓ α∧␈↓"program feature" program written in the style of Algol 60.

␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := w;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := ␈↓NIL␈↓↓;
␈↓ α∧␈↓↓␈↓ αT␈↓ α∧loop:␈↓ αt␈↓αif␈↓↓ null u ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := [␈↓αa␈↓↓ u] . v;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := ␈↓αd␈↓↓ u;
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u6


␈↓ α∧␈↓↓␈↓ αT␈↓ αt␈↓αgo to␈↓↓ loop;


␈↓ α∧␈↓␈↓ αTThe corresponding Elephant program is

␈↓ α∧␈↓↓∀t.[u(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN w
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αd␈↓↓ u(t)
␈↓ α∧␈↓↓␈↓ β4ELSE u(t)],

␈↓ α∧␈↓↓∀t.[v(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αa␈↓↓ u(t) . v(t)
␈↓ α∧␈↓↓␈↓ β4ELSE v(t)]

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 ∧ ¬null u(t) THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTThis can be compared with the LISP program ␈↓↓reverse␈↓ defined by

␈↓ α∧␈↓␈↓ αT␈↓↓reverse u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ reverse ␈↓αd␈↓↓ u * <␈↓αa␈↓↓ u>␈↓.

␈↓ α∧␈↓With␈α∂the␈α∂latter,␈α∂as␈α⊂shown␈α∂in␈α∂(Cartwright␈α∂and␈α∂McCarthy␈α⊂1979),␈α∂it␈α∂is␈α∂convenient␈α∂to␈α⊂prove␈α∂such

␈↓ α∧␈↓properties␈α⊗as␈α∃␈↓↓reverse reverse u = u␈↓␈α⊗and␈α∃␈↓↓reverse[u * v] = reverse v * reverse u␈↓.␈α⊗ The␈α⊗major␈α∃fact

␈↓ α∧␈↓about the Elephant program is expressed by

␈↓ α∧␈↓␈↓ αT␈↓↓∀t0.[pc(t0) = start ⊃ ∃t.[t ≥ t0 ∧ pc(t) = 2 ∧ v(t) = reverse w]]␈↓.

␈↓ α∧␈↓It␈αcan␈αbe␈αproved␈αby␈αproving␈αthat␈α␈↓↓length␈αu(t)␈↓␈αis␈αa␈αdecreasing␈αfunction␈αof␈α␈↓↓t,␈↓␈αi.e.␈αfor␈αany␈α␈↓↓t␈↓␈αsuch␈αthat

␈↓ α∧␈↓␈↓↓pc(t) < 2,␈↓ there is ␈↓↓t' > t␈↓ such that ␈↓↓length u(t') < length t␈↓, and also that

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[reverse w = reverse u(t) * v(t)]␈↓.

␈↓ α∧␈↓This␈α
is␈α
just␈αanother␈α
␈↓↓inductive␈α
assertions␈↓␈α
proof.␈α So␈α
far␈α
it␈α
seems␈αthat␈α
the␈α
most␈αconvenient␈α
technique

␈↓ α∧␈↓for␈αproving␈αfacts␈αabout␈α
Elephant␈αprograms␈αis␈α␈↓↓inductive␈αassertions␈↓,␈α
which␈αis␈αless␈αflexible␈α
than␈αthe

␈↓ α∧␈↓technique␈αdescribed␈αin␈α(Cartwright␈αand␈αMcCarthy␈α1979)␈αthat␈αuses␈αthe␈α␈↓↓functional␈αequation␈↓␈αand␈α
the

␈↓ α∧␈↓␈↓↓minimization␈α
schema␈↓.␈α This␈α
is␈αbecause␈α
␈↓↓inductive␈α
assertions␈↓␈αprovides␈α
no␈αway␈α
of␈αexpressing␈α
algebraic

␈↓ α∧␈↓relations among functions defined by programs.

␈↓ α∧␈↓␈↓ αTOne␈α
mathematically␈α
straightforward␈α
way␈α
of␈α
defining␈α
functions␈α
by␈α
programs␈α
is␈αthe␈α
following.

␈↓ α∧␈↓We␈α
rewrite␈α
the␈α
above␈α
equations␈α
to␈α
introduce␈α
␈↓↓w␈↓␈α
as␈α
an␈α
explicit␈α
argument␈α
of␈α
the␈α
functions␈α
so␈αthat

␈↓ α∧␈↓they become ␈↓↓u(t,w),␈↓ ␈↓↓v(t,w),␈↓ and pc(t,w).  We then define a relation ␈↓↓reverses(v,w)␈↓ by
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u7


␈↓ α∧␈↓␈↓ αT␈↓↓∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))␈↓.

␈↓ α∧␈↓When␈α∂we␈α∂have␈α∞proved␈α∂␈↓↓∀w␈α∂∃!v.reverses(v,w)␈↓,␈α∂first␈α∞order␈α∂logic␈α∂entitles␈α∞us␈α∂to␈α∂replace␈α∂the␈α∞relation

␈↓ α∧␈↓␈↓↓reverses␈↓ by a function.  We can then prove successively that this function satisfies the relations

␈↓ α∧␈↓␈↓ αT␈↓↓reverse ␈↓NIL␈↓↓ = ␈↓NIL␈↓↓␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓reverse [x . u] = reverse u * <x>␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓reverse reverse u = u␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓reverse[u * v] = reverse v * reverese u␈↓,

␈↓ α∧␈↓where the notation is as in (McCarthy and Talcott 1979).




␈↓ α∧␈↓4. ␈↓αAnother Elephant Formalism␈↓

␈↓ α∧␈↓␈↓ αTThe␈α∞Elephant␈α∞formalism␈α∞of␈α∞the␈α∞previous␈α
sections␈α∞sorts␈α∞the␈α∞program␈α∞by␈α∞variables,␈α∞while␈α
a

␈↓ α∧␈↓sequential␈α∞program␈α∂sorts␈α∞it␈α∂according␈α∞to␈α∂the␈α∞program␈α∂counter.␈α∞ The␈α∂latter␈α∞is␈α∂more␈α∞conventional

␈↓ α∧␈↓and␈αoften␈αmore␈αconvenient.␈α
 Moreover,␈αif␈αwe␈αwant␈αto␈α
represent␈αpieces␈αof␈αprogram␈α
separately␈αand

␈↓ α∧␈↓combine them by taking conjunctions, sorting by program counter seems to work better.

␈↓ α∧␈↓␈↓ αTOur pc-sorted Elephant involves three changes:

␈↓ α∧␈↓␈↓ αT1.␈α∞Instead␈α∞of␈α∞writing␈α∞␈↓↓x(t),␈↓␈α∞we␈α∞write␈α∞␈↓↓value(x,t).␈↓␈α∞This␈α∞allows␈α∞us␈α∞to␈α∞quantify␈α∞over␈α∞variables

␈↓ α∧␈↓and is useful for combining the ␈↓αelse␈↓ cases.

␈↓ α∧␈↓␈↓ αT2.␈α∂Instead␈α∂of␈α∂starting␈α∂the␈α∂program␈α∂counter␈α⊂at␈α∂0,␈α∂we␈α∂give␈α∂each␈α∂program␈α∂a␈α⊂symbolic␈α∂entry

␈↓ α∧␈↓location.␈α This␈α
is␈αanalogous␈α
to␈αthe␈α
machine␈αlanguage␈αidea␈α
of␈αa␈α
relocatable␈αprogram,␈α
and␈αit␈αhas␈α
the

␈↓ α∧␈↓same␈αuse.␈α It␈αenables␈αus␈αto␈αcombine␈αprograms␈αby␈αconjunction,␈αand␈αwe␈αcan␈αsuppose␈αthat␈αnumerical

␈↓ α∧␈↓values␈αof␈αthe␈αentry␈αlocations␈αof␈αthe␈αparts␈αof␈αthe␈αprogram␈αare␈αspecified␈αso␈αthat␈αno␈αdistinct␈αparts␈αof

␈↓ α∧␈↓the␈αprograms␈αhave␈αthe␈αsame␈αvalues␈αof␈α
the␈αprogram␈αcounter.␈α Indeed␈αspecifying␈αthe␈αvalues␈α
of␈αthe

␈↓ α∧␈↓entry␈α∀locations␈α∀in␈α∀a␈α∀way␈α∀that␈α∃corresponds␈α∀to␈α∀overlapping␈α∀programs␈α∀will␈α∀usually␈α∀lead␈α∃to␈α∀a

␈↓ α∧␈↓contradiction in the combined sentence.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u8


␈↓ α∧␈↓␈↓ αT3.␈α∩We␈α⊃have␈α∩one␈α∩equation␈α⊃that␈α∩specifies␈α⊃␈↓↓value(var,t+1)).␈↓␈α∩Its␈α∩right␈α⊃side␈α∩is␈α∩a␈α⊃conditional

␈↓ α∧␈↓expression whose clauses correspond to the different values of the program counter.

␈↓ α∧␈↓␈↓ αTWith all these changes, our program ␈↓↓P1␈↓ for multiplication by addition is

␈↓ α∧␈↓↓∀var t.[value(var,t+1) =
␈↓ α∧␈↓↓␈↓ β4IF value(pc,t) = entry1 ∧ var = i THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF value(pc,t) = entry1 + 1 ∧ var = p THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF value(pc,t) = entry1 + 2 ∧ var = pc ∧ value(i,t) = 0 THEN exit1
␈↓ α∧␈↓↓␈↓ β4ELSE IF value(pc,t) = entry1 + 3 ∧ var = i THEN value(i,t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF value(pc,t) = entry1 + 4 ∧ var = p THEN value(p,t) + 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF value(pc,t) = entry1 + 5 ∧ var = pc THEN entry1 + 2

␈↓ α∧␈↓↓␈↓ β4ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 ∧ var = pc THEN value(pc,t) + 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 THEN value(var,t)
␈↓ α∧␈↓↓␈↓ β4ELSE value(var,t+1)␈↓


␈↓ α∧␈↓␈↓ αTNotice␈α
that␈α
there␈αis␈α
one␈α
clause␈α
for␈αeach␈α
statement␈α
in␈α
the␈αAlgol␈α
program␈α
and␈αthree␈α
additional

␈↓ α∧␈↓clauses.␈α
 The␈α
first␈α
additional␈α
clause␈αstates␈α
that␈α
the␈α
program␈α
counter␈αis␈α
increased␈α
by␈α
1␈α
within␈αthe

␈↓ α∧␈↓program␈αunless␈αsomething␈αelse␈αis␈αpreviously␈αstated␈αabout␈αthat␈αvalue␈αof␈αthe␈αprogram␈αcounter.␈α The

␈↓ α∧␈↓second␈αstates␈α
that␈αvariables␈α
whose␈αbehavior␈α
is␈αnot␈α
previously␈αspecified␈α
in␈αthe␈α
program␈αretain␈α
their

␈↓ α∧␈↓values␈α
within␈α
the␈α
program␈α
segment.␈α
 The␈α
last␈α
clause␈α
manages,␈α
by␈α
being␈α
tautologous,␈α
to␈αsay␈α
nothing

␈↓ α∧␈↓about␈αwhat␈αhappens␈αoutside␈αof␈αthe␈αrange␈α␈↓↓entry1 ≤ pc ≤ entry1+5␈↓,␈αthus␈αavoiding␈α
interference␈αwith

␈↓ α∧␈↓sentences specifiying other programs that might be combined with ␈↓↓P1.␈↓

␈↓ α∧␈↓␈↓ αTIndeed␈α
suppose␈α
␈↓↓P2␈↓␈α∞is␈α
another␈α
program␈α∞involving␈α
some␈α
of␈α
the␈α∞same␈α
same␈α
variables␈α∞as␈α
␈↓↓P1␈↓

␈↓ α∧␈↓and␈αpossibly␈αsome␈αothers,␈αand␈αsuppose␈αwe␈αwant␈αto␈αcombine␈αthese␈αprograms␈αso␈αthat␈α␈↓↓P2␈↓␈αis␈α
executed

␈↓ α∧␈↓after␈α∀␈↓↓P1.␈α∀We␈↓␈α∀need␈α∀only␈α∀take␈α∃the␈α∀conjunction␈α∀of␈α∀the␈α∀sentences␈α∀together␈α∀with␈α∃the␈α∀sentence

␈↓ α∧␈↓␈↓↓entry2 = exit1␈↓.␈α∞ Should␈α∞we␈α∂want␈α∞to␈α∞do␈α∂so,␈α∞we␈α∞can␈α∞transform␈α∂the␈α∞conjunction␈α∞into␈α∂an␈α∞equivalent

␈↓ α∧␈↓sentence␈αwhich␈αhas␈αthe␈αsame␈αform␈αas␈α␈↓↓P1␈↓␈αor␈α␈↓↓P2,␈↓␈αi.e.␈αa␈αclause␈αfor␈αeach␈αstatement␈αand␈αthree␈αclauses

␈↓ α∧␈↓at the end.

␈↓ α∧␈↓␈↓ αTCombination␈α∂by␈α∞conjunction␈α∂works␈α∞the␈α∂same␈α∞in␈α∂more␈α∞complicated␈α∂cases.␈α∞ A␈α∂program␈α∞can

␈↓ α∧␈↓have␈αmultiple␈αentries␈α
and␈αexits,␈αany␈αexit␈α
can␈αbe␈αconnected␈αto␈α
any␈αentry␈αjust␈αby␈α
equating␈αsuitable

␈↓ α∧␈↓␈↓↓entry␈↓ and ␈↓↓exit␈↓ parameters.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u9


␈↓ α∧␈↓␈↓ αT5. ␈↓αDefining Functions in Elephant␈↓

␈↓ α∧␈↓␈↓ αTWork␈α
in␈α
program␈α
verification␈α
has␈α
most␈α
often␈α
concerned␈α
itself␈α
with␈α∞verifying␈α
input-output

␈↓ α∧␈↓relations␈α⊂of␈α∂programs,␈α⊂and␈α∂the␈α⊂previous␈α∂section␈α⊂shows␈α∂how␈α⊂to␈α∂do␈α⊂this␈α∂for␈α⊂Elephant␈α∂programs.

␈↓ α∧␈↓Indeed␈α
some␈α
authors␈α
have␈α
left␈α
their␈α
readers␈α
with␈α
the␈α
impression␈α
that␈α
this␈α
is␈α
all␈α
there␈α
is␈αto␈α
program

␈↓ α∧␈↓verification.

␈↓ α∧␈↓␈↓ αTThere␈αis␈α
also␈αproving␈αequivalence␈α
of␈αprogams␈α
in␈αvarious␈αsenses␈α
and␈αproving␈α
properties␈αof

␈↓ α∧␈↓functions␈α
computed␈α
by␈α
programs.␈α
 In␈α
order␈α
to␈α
prove␈α
properties␈α
of␈α
functions␈α
computed␈αby␈α
Elephant

␈↓ α∧␈↓programs, we proceed as follows:

␈↓ α∧␈↓␈↓ αTGiven a relation ␈↓↓P(x,y),␈↓ we can partially define a function ␈↓↓f␈↓ by

␈↓ α∧␈↓␈↓ αT1)␈↓ αt ␈↓↓∀x.(∃y.P(x,y) ⊃ P(x,f(x)))␈↓

␈↓ α∧␈↓␈↓ αTprovided␈α∞␈↓↓f␈↓␈α∞is␈α∞a␈α∞fresh␈α∞function␈α∞symbol.␈α∞ No␈α∞contradiction␈α∞arises␈α∞from␈α∞(1),␈α∞because␈α∂if␈α∞there

␈↓ α∧␈↓isn't␈α
any␈α␈↓↓y␈↓␈α
such␈αthat␈α
␈↓↓P(x,y),␈↓␈αthen␈α
␈↓↓f(x)␈↓␈αis␈α
entirely␈αunrestricted.␈α
 Therefore,␈αnothing␈α
need␈αbe␈α
proved

␈↓ α∧␈↓to␈αentitle␈αus␈αto␈αwrite␈α(1).␈α However,␈αif␈α␈↓↓∀x∃!y.P(x,y)␈↓␈αholds,␈αthen␈α␈↓↓f␈↓␈αis␈αcompletely␈αdetermined,␈αand␈α(1)

␈↓ α∧␈↓can be used to prove its properties.

␈↓ α∧␈↓␈↓ αTWe can use this idea in the Elephant context to write

␈↓ α∧␈↓␈↓ αT2)␈↓ αt␈α␈↓↓∀x.(∃t.(pc(t,x)␈α=␈αdone␈α∧␈α∀t'(t'␈α<␈αt␈α⊃␈αpc(t')␈α≠␈αdone))␈α⊃␈αpc(␈↓	t␈↓↓(x),x)␈α=␈αdone␈α∧␈α∀t'.(t'␈α<␈α␈↓	t␈↓↓(x)

␈↓ α∧␈↓↓⊃ pc(t') ≠ done))␈↓

␈↓ α∧␈↓␈↓ αTthus␈αpartially␈αdefining␈αa␈αfunction␈α␈↓	t␈↓,␈αwhich␈αgives␈αthe␈αtime␈αat␈αwhich␈αthe␈αprogram␈αterminates

␈↓ α∧␈↓as␈α
a␈αfunction␈α
of␈αthe␈α
input␈αparameter␈α
␈↓↓x.␈↓␈αIf␈α
we␈αwant␈α
␈↓↓f(x)␈αto␈↓␈α
be␈αthe␈α
value␈αof␈α
the␈αvariable␈α
␈↓↓y␈↓␈αwhen␈α
the

␈↓ α∧␈↓programs gets to ␈↓↓done,␈↓ we then write

␈↓ α∧␈↓␈↓ αT3)␈↓ αt ␈↓↓∀x.(f(x) = y(␈↓	t␈↓↓(x),x))␈↓.

␈↓ α∧␈↓␈↓ αTWe␈αcan␈αthen␈αuse␈α(2)␈αand␈α(3)␈αto␈αprove␈αany␈αdesired␈αproperties␈αof␈α␈↓↓f.␈↓␈αSome␈αof␈αthese␈αproperties,

␈↓ α∧␈↓including␈α
algebraic␈αrelations␈α
like␈αassociativity␈α
are␈αnot␈α
directly␈αexpressible␈α
as␈αinput-output␈α
relations

␈↓ α∧␈↓of the program.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f10


␈↓ α∧␈↓6. ␈↓αEquivalence of Elephant programs␈↓

␈↓ α∧␈↓␈↓ αTDefinitions␈α&of␈α'the␈α&equivalence␈α'of␈α&Elephant␈α'programs,␈α&equivalence-preserving

␈↓ α∧␈↓transformations␈α∩of␈α⊃programs,␈α∩and␈α⊃techniques␈α∩for␈α⊃proving␈α∩equivalence␈α⊃can␈α∩be␈α⊃expected␈α∩to␈α⊃be

␈↓ α∧␈↓important␈αin␈αapplications.␈α Indeed␈αone␈αapproach␈α
to␈αcompiling␈αis␈αto␈αtransform␈αa␈α
general␈αElephant

␈↓ α∧␈↓program into an immediate program using equivalence-preserving transformations.

␈↓ α∧␈↓␈↓ αTEquivalence␈α
relations␈α
should␈α
be␈α
defined␈α
that␈α
will␈α
facilitate␈α
such␈α
processes.␈α
 An␈α
obvious␈α
form

␈↓ α∧␈↓of␈α
equivalence␈α
is␈α
to␈α
require␈α
that␈α
each␈α
variable␈α
in␈α
the␈α
two␈α
programs␈α
be␈α
represented␈α
by␈α
the␈α
same

␈↓ α∧␈↓function␈α∪of␈α∪time␈α∪for␈α∩all␈α∪values␈α∪of␈α∪the␈α∩parameters.␈α∪ This␈α∪is␈α∪too␈α∩strict␈α∪an␈α∪equivalence␈α∪to␈α∩be

␈↓ α∧␈↓interesting␈α∂on␈α∂two␈α∂grounds.␈α∞ First,␈α∂the␈α∂two␈α∂forms␈α∂of␈α∞the␈α∂multiplication␈α∂by␈α∂addition␈α∂program␈α∞in

␈↓ α∧␈↓section␈α∞2␈α∞would␈α∞not␈α∞be␈α∞equivalent,␈α∞because␈α∞one␈α∞of␈α∞them␈α∞goes␈α∞around␈α∞the␈α∞loop␈α∞in␈α∞one␈α∞time␈α∞step

␈↓ α∧␈↓while␈αthe␈αother␈αtakes␈αfour␈αsteps.␈α Second,␈αtransforming␈αa␈αprogram␈αto␈αan␈αimmediate␈αprogram␈αmay

␈↓ α∧␈↓involve␈α
the␈αintroduction␈α
of␈αnew␈α
variables,␈α
arrays␈αand␈α
other␈αdata␈α
structures␈αin␈α
order␈α
to␈αeliminate

␈↓ α∧␈↓the direct references to the past.

␈↓ α∧␈↓␈↓ αTIn␈α∩fact␈α∩many␈α∩kinds␈α∩of␈α∩equivalence␈α∪are␈α∩useful.␈α∩ We␈α∩begin␈α∩with␈α∩a␈α∩class␈α∪of␈α∩equivalence

␈↓ α∧␈↓relations␈αbased␈αon␈α
a␈αnotion␈αof␈αan␈α
equivalence␈αbetween␈αstates␈αof␈α
two␈αprograms.␈α However,␈αwe␈α
don't

␈↓ α∧␈↓want␈α∂to␈α∂assume␈α∂that␈α∂every␈α∂state␈α∂of␈α∂each␈α∂program␈α∂has␈α∂a␈α∂corresponding␈α∂state␈α∂in␈α∂the␈α⊂other;␈α∂only

␈↓ α∧␈↓certain␈αstates␈α
will␈αcorrespond.␈α
 We␈αcertainly␈α
want␈αthe␈α
beginning␈αand␈α
ending␈αstates␈α
to␈αcorrespond,

␈↓ α∧␈↓and␈α⊂we␈α⊂also␈α⊂want␈α⊂to␈α⊂be␈α⊂sure␈α⊂that␈α⊂any␈α⊂state␈α⊂of␈α⊂one␈α⊂program␈α⊂that␈α⊂corresponds␈α⊂to␈α⊂another␈α⊂will

␈↓ α∧␈↓eventually␈α∞be␈α∞followed␈α∞by␈α∞a␈α∞state␈α∞that␈α∞should␈α∞also␈α∞correspond.␈α∞ Here␈α∞is␈α∞how␈α∞these␈α∞ideas␈α∂can␈α∞be

␈↓ α∧␈↓formalized.

␈↓ α∧␈↓␈↓ αTLet␈α∩one␈α∩Elephant␈α∩program␈α∩␈↓↓P␈↓␈α∩have␈α∩functions␈α∩␈↓↓u␈↓#v1␈↓#(t), ... ,u␈↓#vm␈↓#(t)␈↓␈α∩and␈α∩a␈α∩second␈α∩␈↓↓P'␈↓␈α∩have

␈↓ α∧␈↓functions␈α
␈↓↓u␈↓#v1␈↓#'(t) ... u␈↓#vn␈↓#'(t).␈↓␈α
To␈αavoid␈α
prolixity,␈α
we␈αsummarize␈α
these␈α
functions␈αas␈α
vectors␈α
␈↓↓␈↓αu␈↓↓(t)␈↓␈αand

␈↓ α∧␈↓␈↓↓␈↓αu␈↓↓'(t)␈↓.␈α∪ Let␈α∪␈↓↓EV(␈↓αu␈↓↓,␈↓αu␈↓↓')␈↓␈α∪be␈α∪a␈α∪relation.␈α∪ Let␈α∪␈↓↓P␈↓␈α∪depend␈α∪on␈α∪parameters␈α∪␈↓↓x␈↓#v1␈↓#, ... x␈↓#vp␈↓#␈↓␈α∪and␈α∀␈↓↓P'␈↓␈α∪have

␈↓ α∧␈↓parameters␈α⊃␈↓↓x␈↓#v1␈↓#' ... x␈↓#vq␈↓#'␈↓,␈α⊃similarly␈α⊂summarized␈α⊃into␈α⊃vectors␈α⊂␈↓↓␈↓αx␈↓↓␈↓␈α⊃and␈α⊃␈↓↓␈↓αx␈↓↓'␈↓.␈α⊂ (The␈α⊃parameters␈α⊃of␈α⊂the
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f11


␈↓ α∧␈↓program␈α
for␈αmultiplication␈α
by␈α
addition␈αwere␈α
␈↓↓m␈↓␈αand␈α
␈↓↓n).␈↓␈α
Let␈α␈↓↓EP(␈↓αx␈↓↓,␈↓αx␈↓↓')␈↓␈α
be␈αa␈α
relation␈α
between␈αthe

␈↓ α∧␈↓parameter␈α
vectors.␈α
 Also␈α
let␈α
␈↓↓Q(␈↓αu␈↓↓)␈↓␈α
and␈α
␈↓↓Q'(␈↓αu␈↓↓')␈↓␈αbe␈α
predicates␈α
that␈α
say␈α
what␈α
states␈α
of␈α
the␈αtwo␈α
programs

␈↓ α∧␈↓are to be compared.  Now suppose we can prove that

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ∧ EP(␈↓αx␈↓↓,␈↓αx␈↓↓') ⊃ EV(␈↓αu␈↓↓(0),␈↓αu␈↓↓'(0)) ∧ Q(␈↓αu␈↓↓(0)) ∧ Q'(␈↓αu␈↓↓'(0))␈↓,

␈↓ α∧␈↓i.e. that the initial states of the programs are comparable and correspond, and

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t2 t1'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2 >t1 ∧ Q(␈↓αu␈↓↓(t2)) ⊃ ∃t2'.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓,

␈↓ α∧␈↓i.e.␈α⊂that␈α⊂any␈α⊃comparable␈α⊂state␈α⊂of␈α⊃␈↓↓P␈↓␈α⊂that␈α⊂corresponds␈α⊂to␈α⊃a␈α⊂state␈α⊂of␈α⊃␈↓↓P'␈α⊂is␈↓␈α⊂followed␈α⊃by␈α⊂another

␈↓ α∧␈↓comparable state that corresponds to a state of ␈↓↓P',␈↓

␈↓ α∧␈↓and going the other way

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t1' t2'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2' >t1' ∧ Q'(␈↓αu␈↓↓'(t2')) ⊃ ∃t2.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓.

␈↓ α∧␈↓We␈αshould␈αthen␈αcall␈αthe␈αprograms␈α␈↓↓P␈↓␈αand␈α␈↓↓P'␈↓␈αequivalent␈αwith␈αrespect␈αto␈αthe␈αthe␈αconditions␈α␈↓↓Q␈↓␈αand

␈↓ α∧␈↓␈↓↓Q'␈↓␈αand␈αthe␈αrelations␈α␈↓↓EP␈↓␈αand␈α␈↓↓EV.␈↓␈αNote␈αthat␈αwe␈αhave␈αused␈αthe␈αprograms␈αthemselves␈αas␈αhypotheses

␈↓ α∧␈↓since we can regard a program as the conjunction of its constituent sentences.

␈↓ α∧␈↓␈↓ αTThe two versions of multiplication by addition are equivalent with respect to the predicates

␈↓ α∧␈↓␈↓ αT␈↓↓EP(m,n,m',n') ≡ m=m' ∧ n=n'␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓Q(i,p,pc) ≡ pc = 2 ∨ pc = done␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓Q'(i',p',pc') ≡ pc' = 1 ∨ pc' = done␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨ [i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]␈↓

␈↓ α∧␈↓They␈α∞should␈α∞be␈α∞sufficient␈α∞to␈α∞prove␈α∞that␈α
one␈α∞program␈α∞is␈α∞correct␈α∞(according␈α∞to␈α∞the␈α∞definitions␈α
of

␈↓ α∧␈↓section 2) if and only if the other is.

␈↓ α∧␈↓7. ␈↓αNon Immediate Elephant Programs␈↓

␈↓ α∧␈↓␈↓ αTWhen␈αwe␈αtranslate␈αan␈αAlgol␈αprogram␈αinto␈αElephant,␈αwe␈αget␈αequations␈αin␈αwhich␈α
the␈α␈↓↓x(t+1)␈↓s

␈↓ α∧␈↓depend␈α
only␈α
on␈α
the␈α
␈↓↓x(t)␈↓s.␈α
 We␈α
will␈α
call␈α
such␈α
a␈α
program␈α
an␈α
␈↓↓immediate␈↓␈α
Elephant␈α
program.␈α
 However,
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f12


␈↓ α∧␈↓the␈αrecursion␈αequations␈αwill␈αstill␈αhave␈αguaranteed␈αsolutions␈αif␈αthe␈α␈↓↓x(t)␈↓s␈αdepend␈αon␈αarbitrary␈α
earlier

␈↓ α∧␈↓values of ␈↓↓t.␈↓ This leads to a "high level" programming language with the following features:

␈↓ α∧␈↓␈↓ αT1.␈α∞The␈α
program␈α∞refers␈α∞to␈α
the␈α∞past␈α
through␈α∞earlier␈α∞values␈α
of␈α∞␈↓↓t,␈↓␈α
just␈α∞as␈α∞though␈α
everything

␈↓ α∧␈↓were remembered.

␈↓ α∧␈↓␈↓ αT2.␈α
The␈αcompiler␈α
is␈α
smart␈αand␈α
decides␈αwhat␈α
data␈α
structures␈αare␈α
required␈α
in␈αorder␈α
to␈αcarry␈α
out

␈↓ α∧␈↓the␈α
computations␈α
without␈α
remembering␈α
everything.␈α∞ To␈α
the␈α
extent␈α
that␈α
compilers␈α
can␈α∞be␈α
written

␈↓ α∧␈↓that␈α
do␈α
this␈α
effectively,␈αElephant␈α
is␈α
a␈α
"higher␈α
level"␈αlanguage␈α
in␈α
which␈α
the␈α
programer␈αspecifies␈α
less

␈↓ α∧␈↓than in Algol, etc.



␈↓ α∧␈↓8. ␈↓αAn airline reservation system␈↓

␈↓ α∧␈↓␈↓ αTConsider␈α∃programming␈α∃a␈α⊗trivial␈α∃airline␈α∃reservation␈α∃system.␈α⊗ We␈α∃want␈α∃to␈α∃say␈α⊗that␈α∃␈↓↓a

␈↓ α∧␈↓↓passenger␈α∞has␈α
a␈α∞reservation␈α
if␈α∞he␈α
has␈α∞made␈α∞one␈α
that␈α∞has␈α
not␈α∞been␈α
cancelled␈↓.␈α∞ We␈α
do␈α∞not␈α∞want␈α
to

␈↓ α∧␈↓prescribe␈α∂what␈α⊂data␈α∂structures␈α∂have␈α⊂to␈α∂be␈α∂kept␈α⊂in␈α∂order␈α∂to␈α⊂be␈α∂able␈α∂to␈α⊂answer␈α∂the␈α⊂question␈α∂of

␈↓ α∧␈↓whether someone has a reservation.

␈↓ α∧␈↓␈↓ αTThis␈α∀program␈α∀replies␈α∀properly␈α∀to␈α∀requests␈α∀to␈α∀make␈α∀reservations,␈α∀cancel␈α∀them,␈α∀and␈α∪to

␈↓ α∧␈↓inquiries␈α⊂about␈α∂whether␈α⊂a␈α⊂reservation␈α∂exists.␈α⊂ The␈α∂program␈α⊂refers␈α⊂to␈α∂its␈α⊂input␈α∂in␈α⊂terms␈α⊂of␈α∂an

␈↓ α∧␈↓abstract␈α∀analytic␈α∀syntax␈α∀the␈α∀meaning␈α∀of␈α∀whose␈α∀mnemonic␈α∀predicate␈α∀and␈α∀function␈α∀names␈α∀is

␈↓ α∧␈↓hopefully␈αobvious.␈α The␈αonly␈αdata␈αstructure␈αexplicitly␈αmentioned␈αis␈αthe␈αnumber␈αof␈α
seats␈αcurrently

␈↓ α∧␈↓occupied,␈α
and␈α
even␈α
that␈α
could␈α
be␈αeliminated␈α
from␈α
the␈α
program.␈α
 The␈α
Elephant␈αcompiler,␈α
therefore,

␈↓ α∧␈↓gets␈αthe␈α
honor␈αof␈α
determining␈αwhat␈α
other␈αdata␈α
structures␈αare␈α
needed.␈α We␈α
use␈αthe␈α
convention␈αof

␈↓ α∧␈↓writing ␈↓↓{x}f␈↓ instead of ␈↓↓f(x)␈↓ when it is convenient to write the argument before the function name.

␈↓ α∧␈↓↓␈↓ αT∀t.[output(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You had it"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE IF number(t) = N THEN "No room"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You have it now"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "It's cancelled"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have it to cancel"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF isinquiry in THEN␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You have one"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have one"]
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f13


␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓␈↓ αT∀t.[number(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) ∨ number(t) = N
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$THEN number(t)
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t) + 1]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN number(t) - 1
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t)]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE number(t)]

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[hasrev(passenger,t)␈α∂≡␈α∂∃t1.(t1␈α∂<␈α∂t␈α∂∧␈α∂ismake␈α∞input␈α∂t1␈α∂∧␈α∂passenger␈α∂=␈α∂maker␈α∂input␈α∂t1␈α∞∧

␈↓ α∧␈↓↓number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧ iscancel input t2 ∧ maker input t2 = passenger))]␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α⊃main␈α∩difficulty␈α⊃in␈α⊃making␈α∩a␈α⊃compiler␈α∩for␈α⊃Elephant␈α⊃is␈α∩illustrated␈α⊃by␈α∩the␈α⊃predicate

␈↓ α∧␈↓␈↓↓hasrev.␈↓␈α∞The␈α∂compiler␈α∞has␈α∞to␈α∂understand␈α∞that␈α∂it␈α∞must␈α∞remember␈α∂successful␈α∞reservations␈α∂but␈α∞can

␈↓ α∧␈↓forget␈αunsuccessful␈αattempts␈αat␈αmaking␈αa␈αreservation␈αand␈αthat␈αit␈αcan␈αforget␈αreservations␈αthat␈αhave

␈↓ α∧␈↓been␈α
cancelled.␈α Perhaps␈α
␈↓↓hasrev␈↓␈αshould␈α
be␈αwritten␈α
using␈α
primitives␈αthat␈α
refer␈αexplicitly␈α
to␈αthe␈α
most

␈↓ α∧␈↓recent occurrence of an event, which might permit a less intelligent compiler.

␈↓ α∧␈↓9. ␈↓αParallel processes for computing a sum of functions␈↓

␈↓ α∧␈↓␈↓ αTThe␈α∃following␈α∃Elephant␈α⊗program␈α∃computes␈α∃␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓␈α⊗using␈α∃␈↓↓k␈↓␈α∃processors.␈α⊗ A␈α∃master

␈↓ α∧␈↓processor␈α⊃with␈α⊃program␈α⊂counter␈α⊃␈↓↓pc(t)␈↓␈α⊃initializes␈α⊂the␈α⊃variables␈α⊃␈↓↓n␈↓␈α⊂and␈α⊃␈↓↓s␈↓␈α⊃and␈α⊂starts␈α⊃the␈α⊃␈↓↓k␈↓␈α⊂slave

␈↓ α∧␈↓processes␈α
whose␈α
program␈α
counters␈α
are␈α
written␈α
␈↓↓pc(i,t)␈↓␈αat␈α
step␈α
1.␈α
 A␈α
process␈α
needs␈α
exclusive␈αaccess␈α
to

␈↓ α∧␈↓␈↓↓n␈↓␈αwhen␈αreading␈αand␈α
incrementing␈αit,␈αneed␈αexclusive␈α
access␈αto␈α␈↓↓s␈↓␈αwhen␈α
incrementing␈αit,␈αand␈αwe␈α
only

␈↓ α∧␈↓provide␈α
for␈αexclusive␈α
access␈αat␈α
these␈αtimes.␈α
 We␈α
presuppose␈αthat␈α
computing␈α␈↓↓f(n)␈↓␈α
takes␈α␈↓↓time(n)␈↓␈α
units

␈↓ α∧␈↓of␈α∞time,␈α∞and␈α∞these␈α∞operations␈α∞are␈α∞done␈α∞in␈α∞parallel.␈α∞ ␈↓↓pc(t)␈↓␈α∞is␈α∞the␈α∞program␈α∞counter␈α∞for␈α∞the␈α
master

␈↓ α∧␈↓process,␈αand␈α
␈↓↓pc(i,t)␈↓␈αis␈α
the␈αprogram␈α
counter␈αof␈αthe␈α
␈↓↓i␈↓th␈αslave␈α
process.␈α The␈α
updating␈αof␈αall␈α
variables

␈↓ α∧␈↓except␈α⊂the␈α∂␈↓↓pc(i,t)␈↓␈α⊂works␈α∂as␈α⊂in␈α∂Algolic␈α⊂programs,␈α∂but␈α⊂the␈α∂latter␈α⊂requires␈α∂a␈α⊂more␈α⊂elaborate␈α∂and

␈↓ α∧␈↓somewhat implicit description that may well challenge the designer of an Elephant compiler.

␈↓ α∧␈↓↓n(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
␈↓ α∧␈↓↓␈↓ β∀ELSE n(t)
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f14


␈↓ α∧␈↓↓s(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
␈↓ α∧␈↓↓␈↓ β∀ELSE s(t)

␈↓ α∧␈↓↓m(i,t+1)␈↓ αz= ␈↓ β∀IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
␈↓ α∧␈↓↓␈↓ β∀ELSE m(i,t)

␈↓ α∧␈↓↓pc(t+1) ␈↓ αz= ␈↓ β∀IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE pc(t) + 1


␈↓ α∧␈↓↓pc(i,0) = 0

␈↓ α∧␈↓↓pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

␈↓ α∧␈↓↓pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

␈↓ α∧␈↓↓pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3
␈↓ α∧␈↓↓␈↓ β∀⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

␈↓ α∧␈↓↓pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

␈↓ α∧␈↓↓pc(i,t) = 5 ⊃ pc(i,t+1) = 1

␈↓ α∧␈↓␈↓ αTIt␈α∩may␈α∪be␈α∩questioned␈α∪whether␈α∩the␈α∪above␈α∩Elephant␈α∪program␈α∩should␈α∪be␈α∩regarded␈α∪as␈α∩a

␈↓ α∧␈↓"program"␈α∞that␈α∞can␈α
be␈α∞compiled␈α∞by␈α∞a␈α
suitable␈α∞compiler␈α∞or␈α
as␈α∞something␈α∞between␈α∞a␈α
specification

␈↓ α∧␈↓and␈αa␈α
program.␈α Perhaps␈α
it␈αis␈α
an␈αexample␈α
of␈αthat␈α
elusive␈αconcept␈α
called␈αan␈α
algorithm.␈α Notice␈α
that

␈↓ α∧␈↓it␈α
assumes␈αthat␈α
synchronization␈αoccurs␈α
without␈αspecifying␈α
any␈αway␈α
of␈αdoing␈α
it.␈α Just␈α
the␈α
thing␈αto

␈↓ α∧␈↓challenge␈αa␈αsmart␈αcompiler␈α
or␈αautomatic␈αprogramming␈αsystem.␈α
 On␈αthe␈αother␈αhand,␈αthe␈α
correctness

␈↓ α∧␈↓of the Elephant program is given by the statement,

␈↓ α∧␈↓␈↓↓∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = ␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓

␈↓ α∧␈↓and␈α∀this␈α∀can␈α∃presumably␈α∀be␈α∀proved␈α∀from␈α∃the␈α∀program.␈α∀ The␈α∀correspondence␈α∃between␈α∀this

␈↓ α∧␈↓Elephant␈α⊗program␈α∃and␈α⊗one␈α∃that␈α⊗is␈α∃more␈α⊗explicit␈α∃about␈α⊗synchronization␈α∃might␈α⊗be␈α∃proved

␈↓ α∧␈↓separately.

␈↓ α∧␈↓␈↓ αTThere may well be better ways of describing parallel processes in Elephant.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f15


␈↓ α∧␈↓10. ␈↓αTemporal Logic Considered Unnecessary␈↓

␈↓ α∧␈↓{t| P(t}

␈↓ α∧␈↓x is increasing with time

␈↓ α∧␈↓P is true until the first time Q is true

␈↓ α∧␈↓Relations␈α
between␈α
values␈α
of␈αthe␈α
variables␈α
at␈α
different␈α
times␈αcan␈α
be␈α
expressed␈α
in␈α
temporal␈αlogic␈α
but

␈↓ α∧␈↓only with extra quantifiers.

␈↓ α∧␈↓␈↓ αTThe␈α∞Elephant␈α∞approach␈α∂to␈α∞representing␈α∞programs␈α∞and␈α∂proving␈α∞their␈α∞properties␈α∞is␈α∂a␈α∞close

␈↓ α∧␈↓relative␈α⊂of␈α⊂the␈α⊂modal␈α⊃logic␈α⊂approach␈α⊂of␈α⊂(Pnueli␈α⊂1978)␈α⊃and␈α⊂(Manna␈α⊂and␈α⊂Pnueli␈α⊃1979).␈α⊂ Their

␈↓ α∧␈↓formalism␈α⊂also␈α⊂explicitly␈α∂refers␈α⊂to␈α⊂the␈α∂values␈α⊂of␈α⊂the␈α∂program␈α⊂counter␈α⊂but␈α∂treats␈α⊂it␈α⊂in␈α∂formally

␈↓ α∧␈↓different␈α∂way␈α∂from␈α∞ordinary␈α∂program␈α∂variables.␈α∂ However,␈α∞instead␈α∂of␈α∂representing␈α∂variables␈α∞as

␈↓ α∧␈↓functions␈α
of␈α
time,␈α
they␈α
use␈αtemporal␈α
operators␈α
␈↓↓F␈↓␈α
(eventually),␈α
␈↓↓G␈↓␈α
(for␈αall␈α
future␈α
times)␈α
and␈α
␈↓↓X␈↓␈α(at␈α
the

␈↓ α∧␈↓next␈α∞time).␈α
 (This␈α∞is␈α
Pnueli's␈α∞notation,␈α
the␈α∞joint␈α
paper␈α∞uses␈α
the␈α∞qD,␈α
qN␈α∞common␈α
in␈α∞modal␈α
logic

␈↓ α∧␈↓together with qO for ␈↓↓X).  ␈↓ The modal logic is justified in (Manna and Pnueli 1979) as follows:

␈↓ α∧␈↓␈↓ αT␈↓↓"In␈αspite␈α
of␈αthese␈αqualifications␈α
there␈αare␈αsome␈α
obvious␈αadvantages␈αin␈α
the␈αintroduction␈αand␈α
use

␈↓ α∧␈↓↓of␈α∞modal␈α∂formalisms.␈α∞ It␈α∂allows␈α∞an␈α∂explicit␈α∞discrimination␈α∂of␈α∞one␈α∂parameter␈α∞as␈α∂being␈α∞appreciably

␈↓ α∧␈↓↓more␈α↔significant␈α↔than␈α_all␈α↔the␈α↔others,␈α↔and␈α_makes␈α↔dependence␈α↔on␈α↔that␈α_parameter␈α↔implicit.

␈↓ α∧␈↓↓Nowadays,␈α∩when␈α∩increasing␈α∩attention␈α∩is␈α∩paid␈α∩to␈α∩the␈α∩clear␈α∩correspondence␈α∩between␈α∪syntax␈α∩and

␈↓ α∧␈↓↓natural␈αreasoning␈α(as␈αis␈αrepeatedly␈αstressed␈αby␈αthe␈αdiscipline␈αof␈αStructured␈αProgramming),␈αit␈αseems

␈↓ α∧␈↓↓only␈α∂appropriate␈α∂to␈α∂introduce␈α∞extra␈α∂structure␈α∂into␈α∂the␈α∞description␈α∂of␈α∂varying␈α∂situations.␈α∂ Thus␈α∞a

␈↓ α∧␈↓↓clear␈α
distinction␈α
is␈α
made␈α
between␈α
variation␈α
within␈αa␈α
state,␈α
which␈α
we␈α
express␈α
using␈α
predicates␈αand

␈↓ α∧␈↓↓quantifiers, and variation from one state to another, which we express using modal operators"␈↓.

␈↓ α∧␈↓␈↓ αTManna␈α
and␈α
Pnueli␈α
are␈α
right␈α
in␈αasserting␈α
that␈α
in␈α
programming␈α
variation␈α
in␈α
time␈αis␈α
especially

␈↓ α∧␈↓significant.␈α⊃ Unfortunately,␈α⊃expressing␈α∩temporal␈α⊃variation␈α⊃with␈α∩modal␈α⊃operators␈α⊃makes␈α∩time␈α⊃a

␈↓ α∧␈↓second␈α⊂class␈α⊂citizen␈α⊂and␈α⊂limits␈α⊂what␈α⊂can␈α⊂be␈α⊂conveniently␈α⊂said␈α⊂about␈α⊂it.␈α⊂ Let␈α⊂us␈α⊂compare␈α∂some

␈↓ α∧␈↓Elephant assertions with the corresponding assertions in temporal logic.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f16


␈↓ α∧␈↓1. Total correctness of a program

␈↓ α∧␈↓␈↓ αT␈↓↓∀t ␈↓	F␈↓↓(x(t)) ⊃ ∃t'.(t' > t ∧ pc(t') = done ∧ qP(x(t),x(t'))␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(x) ∧ x = a ⊃ F [at done ∧ qP(a,x)]␈↓

␈↓ α∧␈↓2. Partial correctness of a program

␈↓ α∧␈↓␈↓ αT␈↓↓∀t t'.

␈↓ α∧␈↓The␈α
following␈α
examples␈α
taken␈α∞from␈α
(Manna␈α
and␈α
Pnueli␈α
1979)␈α∞Kamp␈α
defined␈α
two␈α
tenses␈α∞by␈α
the

␈↓ α∧␈↓equivalences:

␈↓ α∧␈↓p S q ≡ (∃t){t < n ∧ q(t) ∧ (∀t')[t < t' < n) ⊃ p(t')]}

␈↓ α∧␈↓p T q ≡ (∃t){n < t ∧ q(t) ∧ (∀t')[n < t' < t) ⊃ p(t')]}

␈↓ α∧␈↓Here␈α␈↓↓p␈αS␈αq␈↓␈αis␈αread␈α"␈↓↓p␈↓␈αsince␈α␈↓↓q␈↓␈α",␈αand␈α␈↓↓p␈αT␈αq␈↓␈αis␈αread␈α"␈↓↓p␈↓␈αtill␈α␈↓↓q␈↓␈α".␈αKamp␈α(1968)␈αproved␈αthat␈αfor␈αdense

␈↓ α∧␈↓time,␈αinfinite␈αin␈αboth␈αdirections,␈α␈↓↓S␈↓␈αand␈α␈↓↓T␈↓␈αare␈αnot␈αdefinable␈αin␈αterms␈αof␈αany␈αunary␈αtenses␈αand␈αthat

␈↓ α∧␈↓all␈α
"tenses"␈αcan␈α
be␈α
defined␈αin␈α
terms␈α
of␈α␈↓↓S␈↓␈α
and␈α
␈↓↓T.␈↓␈αWhile␈α
this␈α
doesn't␈αshow␈α
that␈α
␈↓↓S␈↓␈αand␈α
␈↓↓T␈↓␈α
can't␈αbe

␈↓ α∧␈↓defined␈α
in␈αterms␈α
of␈αunary␈α
tenses␈αfor␈α
integer␈αtime,␈α
I'll␈α
be␈αthey␈α
can't.␈α Moreover,␈α
␈↓↓T␈↓␈αwould␈α
seem␈αto␈α
be

␈↓ α∧␈↓an entirely relevant tense for proramming.  It says that ␈↓↓p␈↓ will be true until ␈↓↓q␈↓ becomes true.



␈↓ α∧␈↓11. ␈↓αRemarks␈↓

␈↓ α∧␈↓1.␈αPrograms␈αin␈αLucid␈α(Ashcroft␈αand␈αWadge␈α1976)␈αare␈αalso␈αcollections␈αof␈αsentences␈αin␈αa␈αfirst␈αorder

␈↓ α∧␈↓language.␈α A␈αLucid␈αobject␈αis␈αa␈αvector␈α
of␈αthe␈αvalues␈αof␈αa␈αvariable␈αthroughout␈αtime.␈α
 This␈αpermits

␈↓ α∧␈↓some␈α
statements␈α∞to␈α
be␈α∞made␈α
in␈α∞a␈α
very␈α∞neat␈α
way.␈α
 However,␈α∞it␈α
seems␈α∞to␈α
be␈α∞less␈α
flexible␈α∞than␈α
the

␈↓ α∧␈↓Elephant␈α∞device␈α∞of␈α∞admitting␈α∞the␈α∞time␈α∞as␈α∞an␈α∞explicit␈α∞parameter.␈α∞ Lucid␈α∞programs␈α∞do␈α∞not␈α∞admit

␈↓ α∧␈↓␈↓αgo to␈↓s,␈αand␈α
there␈αare␈α
other␈αunexpected␈α
restrictions.␈α Perhaps␈α
some␈αof␈α
Lucid's␈αproblems␈α
would␈αbe

␈↓ α∧␈↓cured by including the history of the program counter as a variable.

␈↓ α∧␈↓2.␈αThe␈αproperties␈αof␈αElephant␈αprograms␈αdon't␈αdepend␈αon␈αtime␈αtaking␈αinteger␈αvalues.␈α All␈αwe␈αneed

␈↓ α∧␈↓require␈αis␈αthat␈αthe␈αset␈αof␈αtimes␈αbe␈αordered␈αand␈αunbounded␈αabove.␈α Then␈αthe␈αfirst␈αsentence␈αof␈αthe

␈↓ α∧␈↓product program would take the form
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f17


␈↓ α∧␈↓␈↓↓∀t ∃t'.[t' > t ∧ i(t') ␈↓ ∧~= ␈↓ ∧4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧4ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ ∧4ELSE i(t)].

␈↓ α∧␈↓3.␈α∂It␈α∞seems␈α∂to␈α∂me␈α∞that␈α∂any␈α∂language␈α∞that␈α∂purports␈α∞to␈α∂allow␈α∂the␈α∞user␈α∂to␈α∂say␈α∞what␈α∂he␈α∂wants␈α∞the

␈↓ α∧␈↓computer␈αto␈α
do␈αin␈α
English,␈αshould␈α
allow␈αthe␈α
executive␈αor␈αgeneral␈α
or␈αother␈α
big␈αshot␈α
to␈αsay␈α
that␈α␈↓↓a

␈↓ α∧␈↓↓customer␈αhas␈αa␈αreservation␈αif␈αhe␈αhas␈αmade␈αone␈αand␈αit␈αhasn't␈αbeen␈αcancelled␈↓.␈α The␈αbig␈αshot␈αcertainly

␈↓ α∧␈↓doesn't␈α⊂want␈α⊂to␈α∂concern␈α⊂himself␈α⊂with␈α⊂what␈α∂data␈α⊂structures␈α⊂are␈α⊂required␈α∂in␈α⊂order␈α⊂to␈α⊂fulfill␈α∂his

␈↓ α∧␈↓wishes,␈α∩and␈α∪Elephant␈α∩shows␈α∩that␈α∪his␈α∩wishes␈α∩can␈α∪be␈α∩stated␈α∩without␈α∪mentioning␈α∩such␈α∪a␈α∩data

␈↓ α∧␈↓structure.

␈↓ α∧␈↓4.␈α∂In␈α∂its␈α∂present␈α∂state,␈α∂Elephant␈α∞doesn't␈α∂seem␈α∂to␈α∂be␈α∂a␈α∂very␈α∞easy␈α∂language␈α∂to␈α∂use.␈α∂ I␈α∂say␈α∞"seem",

␈↓ α∧␈↓because␈αthe␈αawkward␈αprograms␈αmay␈αbe␈αmerely␈αa␈αconsequence␈αof␈αinexperience.␈α Of␈αcourse,␈αAlgolic

␈↓ α∧␈↓programs␈α∂can␈α∂easily␈α∂be␈α∞translated␈α∂into␈α∂Elephant,␈α∂but␈α∞this␈α∂doesn't␈α∂take␈α∂advantage␈α∂of␈α∞Elephant's

␈↓ α∧␈↓ability to refer directly to the past.

␈↓ α∧␈↓5.␈α∞Regarded␈α
simply␈α∞as␈α∞a␈α
way␈α∞of␈α
writing␈α∞Algolic␈α∞programs␈α
as␈α∞logical␈α
sentences,␈α∞Elephant␈α∞plays␈α
a

␈↓ α∧␈↓role␈α⊃similar␈α⊂to␈α⊃that␈α⊃played␈α⊂by␈α⊃the␈α⊃Cartwright␈α⊂way␈α⊃of␈α⊃writing␈α⊂Lisp␈α⊃style␈α⊃recursive␈α⊂conditional

␈↓ α∧␈↓expression␈α∂programs␈α∂as␈α⊂logical␈α∂sentences.␈α∂ In␈α⊂fact␈α∂it␈α∂may␈α⊂be␈α∂a␈α∂kind␈α⊂of␈α∂dual␈α∂to␈α⊂the␈α∂Cartwright

␈↓ α∧␈↓method␈α∂just␈α∂as␈α∂␈↓↓inductive␈α∞assertions␈↓␈α∂and␈α∂␈↓↓subgoal␈α∂induction␈↓␈α∞seem␈α∂to␈α∂be␈α∂duals.␈α∂ Namely,␈α∞Elephant

␈↓ α∧␈↓programs␈αand␈αinductive␈αassertions␈αwork␈αfrom␈αan␈αinitial␈αstate␈αand␈αdescribe␈αits␈αchanges,␈αwhile␈αLisp

␈↓ α∧␈↓style␈α∂programs␈α∂and␈α∂subgoal␈α∂induction␈α∂work␈α∂backwards␈α∂from␈α∂desired␈α∂final␈α∂result.␈α∂ Thus␈α∂it␈α∂may

␈↓ α∧␈↓complete a pattern of methods of program formalization.

␈↓ α∧␈↓6.␈α∞Elephant␈α∞may␈α∞be␈α∞expanded␈α∞by␈α∞relaxing␈α∞the␈α∞restriction␈α∞that␈α∞statements␈α∞refer␈α∞only␈α∞to␈α∞the␈α
past.

␈↓ α∧␈↓Our␈α⊂big␈α⊂shot␈α∂may␈α⊂wish␈α⊂to␈α∂say,␈α⊂␈↓↓"When␈α⊂the␈α⊂passengers␈α∂arrive␈α⊂at␈α⊂the␈α∂airport␈α⊂for␈α⊂the␈α⊂flight,␈α∂an

␈↓ α∧␈↓↓airplane␈α⊃and␈α⊂a␈α⊃crew␈α⊃will␈α⊂have␈α⊃been␈α⊃summoned␈α⊂by␈α⊃the␈α⊂scheduling␈α⊃program␈α⊃to␈α⊂fly␈α⊃them␈α⊃to␈α⊂their

␈↓ α∧␈↓↓destination"␈↓.␈α∞ Allowing␈α
the␈α∞right␈α
hand␈α∞sides␈α
of␈α∞Elephant␈α
equations␈α∞to␈α
refer␈α∞to␈α
the␈α∞future␈α∞puts␈α
a

␈↓ α∧␈↓heavier␈αburden␈αon␈αthe␈αcompiler.␈α In␈α
fact,␈αmany␈αfuturistic␈αElephant␈αprogram␈αare␈αcontradictory␈α
and
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f18


␈↓ α∧␈↓hence␈α
uncompilable.␈α Thus␈α
a␈αcompiler␈α
for␈α
futuristic␈αElephant␈α
is␈αreally␈α
a␈αkind␈α
of␈α
problem␈αsolver.

␈↓ α∧␈↓Nevertheless, this style of programming may prove practicaly useful and theoretically illuminating.

␈↓ α∧␈↓8.␈αChurch␈α(1957)␈αrepresents␈αdigital␈αcircuits␈αas␈αrecursive␈αsystems␈αof␈αBoolean␈αequations␈αdetermining

␈↓ α∧␈↓the␈αbehavior␈α
of␈αa␈α
collection␈αof␈α
Boolean␈αvariables␈αas␈α
a␈αfunction␈α
of␈αtime.␈α
 He␈αdiscusses␈αthe␈α
synthesis

␈↓ α∧␈↓of␈α⊂circuits␈α⊂with␈α⊂given␈α⊂behavior.␈α⊂ Some␈α⊂of␈α⊃his␈α⊂results␈α⊂might␈α⊂lead␈α⊂to␈α⊂theorems␈α⊂about␈α⊃classes␈α⊂of

␈↓ α∧␈↓Elephant programs over finite domains in cases where the finiteness of the domain is important.



␈↓ α∧␈↓12. ␈↓αReferences␈↓

␈↓ α∧␈↓␈↓αAshcroft,␈α∞E.␈α∞A.␈α∞and␈α∞W.␈α∞W.␈α∞Wadge␈α∞(1976)␈↓:␈α∞Lucid␈α∞-␈α∞A␈α∞Formal␈α∞System␈α∞for␈α∞Writing␈α∞and␈α∞Proving

␈↓ α∧␈↓Programs, ␈↓↓SIAM Journal of Computing␈↓, Vol. 5, No. 3, September.

␈↓ α∧␈↓␈↓αBurgess, John P. (1979)␈↓: "Logic and Time", ␈↓↓Journal of Symbolic Logic␈↓, vol. 44, No. 4, Dec. 1979.

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1976)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed

␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ α∧␈↓␈↓αCartwright,␈α⊃Robert␈α⊂and␈α⊃John␈α⊂McCarthy␈α⊃(1979)␈↓:␈α⊃"Recursive␈α⊂Programs␈α⊃as␈α⊂Functions␈α⊃in␈α⊃a␈α⊂First

␈↓ α∧␈↓Order␈α
Theory",␈α
in␈α
E.␈α
Blum␈α
and␈α
S.␈αTakasu␈α
(eds.),␈α
␈↓↓Proceedings␈α
of␈α
the␈α
International␈α
Conference␈αon

␈↓ α∧␈↓↓Mathematical Studies of Information Processing␈↓, Springer Publishers.

␈↓ α∧␈↓␈↓αChurch,␈αAlonzo␈α(1957)␈↓:␈α
"Application␈αof␈αRecursive␈α
Arithmetic␈αto␈αthe␈α
Problem␈αof␈αCircuit␈α
Synthesis",

␈↓ α∧␈↓in␈α∞␈↓↓Summaries␈α∞of␈α∂talks␈α∞presented␈α∞at␈α∂the␈α∞Summer␈α∞Institute␈α∂for␈α∞Symbolic␈α∞Logic,␈α∂Cornell␈α∞University

␈↓ α∧␈↓↓1957␈↓., Institute for Defense Analyses.

␈↓ α∧␈↓␈↓αFrancez,␈α↔Nissim␈α↔and␈α⊗Amir␈α↔Pnueli␈α↔(1978)␈↓:␈α⊗"A␈α↔Proof␈α↔Method␈α⊗for␈α↔Cyclic␈α↔Programs",␈α⊗␈↓↓Acta

␈↓ α∧␈↓↓Informatica␈↓ 9, 133-157.

␈↓ α∧␈↓␈↓αFrancez,␈α⊃Nissim␈α⊂(1976)␈↓:␈α⊃␈↓↓The␈α⊂Analysis␈α⊃of␈α⊂Cyclic␈α⊃Programs␈↓,␈α⊂PhD␈α⊃Thesis,␈α⊂Weizmann␈α⊃Institute␈α⊂of

␈↓ α∧␈↓Science, Rehovot, Israel.

␈↓ α∧␈↓␈↓αFrancez,␈α∞Nissim␈α∂(1978)␈↓:␈α∞"An␈α∂Application␈α∞of␈α∂a␈α∞Method␈α∂for␈α∞Analysis␈α∂of␈α∞Cyclic␈α∂Programs",␈α∞␈↓↓IEEE

␈↓ α∧␈↓↓Transactions on Software Engineering␈↓, vol. SE-4, No. 5, pp. 371-378, September 1978.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f19


␈↓ α∧␈↓␈↓αKamp, Hans (1968)␈↓: ␈↓↓On Tense Logic and the Theory of Order␈↓, PhD Thesis, U.C.L.A.

␈↓ α∧␈↓␈↓αKroger,␈αF.␈α(1978)␈↓:␈α"A␈αUniform␈αLogical␈αBasis␈αfor␈αthe␈αDescription,␈αSpecification␈αand␈αVerification␈α
of

␈↓ α∧␈↓Programs", in E.J. Neuhold (ed.),

␈↓ α∧␈↓␈↓αManna,␈α∂Zohar␈α∂and␈α∂Amir␈α∂Pnueli␈α∂(1979)␈↓:␈α⊂␈↓↓The␈α∂Modal␈α∂Logic␈α∂of␈α∂Programs␈↓,␈α∂preliminary␈α⊂version␈α∂of

␈↓ α∧␈↓technical␈α∩report,␈α∪Computer␈α∩Science␈α∪Department,␈α∩Stanford␈α∪University.␈α∩ ␈↓↓Formal␈α∪Descriptions␈α∩of

␈↓ α∧␈↓↓Programming Concepts␈↓, North-Holland.

␈↓ α∧␈↓␈↓αMcCarthy, John and Carolyn Talcott (1980)␈↓: ␈↓↓LISP: Programming and Proving␈↓, (in preparation)

␈↓ α∧␈↓␈↓αPnueli,␈α
A.␈α
(1978)␈↓:␈α∞␈↓↓The␈α
Temporal␈α
Semantics␈α
of␈α∞Concurrent␈α
Programs␈↓,␈α
Technical␈α∞Report,␈α
Tel-Aviv

␈↓ α∧␈↓University.

␈↓ α∧␈↓␈↓αPrior, A. N. (1967)␈↓: ␈↓↓Past, Present and Future␈↓, Oxford.

␈↓ α∧␈↓␈↓αRescher,␈α⊂Nicholas␈α⊂and␈α∂Alasdair␈α⊂Urquhart␈α⊂(1971)␈↓:␈α∂␈↓↓Temporal␈α⊂Logic␈↓,␈α⊂Springer-Verlag,␈α⊂New␈α∂York

␈↓ α∧␈↓and Vienna.


␈↓ α∧␈↓This partial draft of ELEPHA[S80,JMC] compiled at 17:00 on April 29, 1981.